(TML)
"X:*";;
"Y:**";;
"F:*->(**->**)";;
"P:*->tr";;
"C:*->(**->(**->**))";;
"G:*->*";;
"H:**->**";;

let fun = "\F X Y. C X Y (F (G X) (H Y))";;
let deff = "F == FIX ↑fun" ;;
              % ↑fun donne la "valeur" de fun ... antiquote %
let assh = "H UU == UU" ;;
let assch = "!X Y Z. H (C X Y Z) == C X (H Y) (H Z)";;

let deffthm = ASSUME deff ;;
let asshthm = ASSUME assh ;;       
let asschthm = ASSUME assch ;;

let wgoalf = "!X Y. H(F X Y) == F X (H Y)" ;;

let ssf = itlist ssadd [asshthm;asschthm] BASICSS ;;

let goalf = (wgoalf,ssf,[deff;assh;assch]);;


let GREUTAC ((w,ss,fml):goal) =
  ([w,itlist ssadd (map ASSUME fml) ss,fml],hd);;

let TACTICF = INDUCTAC [deffthm] THEN SIMPTAC THEN (REPEAT GENTAC)
              THEN GREUTAC THEN SIMPTAC;;